D:Dsys, L:Id List, f:(IdType).
(i:Id. (i  L)  M(i) =   MsgA)
 (iL. l:IdLnk, tg:Id. rcv(l,tg) declared in M(i)  M(i).da(rcv(l,tg)) = f(tg)  Type)
 (i:Id. Feasible(M(i)))
 Feasible(D) 

latex

Definitions

x:A. B(x), P  Q, P  Q, t  T, P  Q, P  Q, Prop, x. t(x), P & Q, xL. P(x), 1of(t), interface-check(D;l;tg;T), 2of(t), rcv(l,tg) declared in M, M.da(a), ma-outlinks(M;i), True, T, SQType(T), {T}, Top, x(s), Dec(P), MsgA, M.din(l,tg), Valtype(da;k), da-outlinks(da;i), A & B, x:A. B(x), Knd, da-outlink-f(da;k), b, isrcv(k), lnk(k), tag(k), isl(x), true, false, if b t else f fi, False, outl(x), SqStable(P), f(x)?z, A, rcv(l,tg)

Lemmas

finite-support-feasible, all functionality wrt iff, l member wf, assert wf, ma-is-empty wf, d-m wf, msga wf, ma-empty wf, or functionality wrt iff, assert-ma-is-empty, Id wf, ma-feasible wf, l all wf, IdLnk wf, ma-declm wf, ma-da wf, rcv wf, dsys wf, ldst wf, pi1 wf, ma-outlinks wf, decidable ma-declm, fpf-dom wf, Knd wf, Kind-deq wf, fpf-trivial-subtype-top, fpf-cap wf, top wf, da-outlinks wf, member map filter, has-src wf, da-outlink-f wf, assert-has-src, isrcv wf, fpf-dom-list wf, pi2 wf, sq stable from decidable, decidable assert, bool cases, bool sq, bool wf, eqtt to assert, iff transitivity, bnot wf, not wf, eqff to assert, assert of bnot, Id sq, din-not-declared